x,y:int_seg(0; 3). (rps(x; y))  (x = y  )  (rps(y; x)) 

latex

Definitions

i z j, #$n, sqequal(s; t), sq_type(T), guard(T), SqStable(P), ff, tt, decidable(P), rps(x; y), Unit, P  Q, x:A  B(x), P  Q, T, b, i <z j, True, prop{i:l}, Type, , False, P  Q, left + right, x:A. B(x), x:AB(x), t  T, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), if a=b  then c  else d, int_seg(i; j), {x:A| B(x)} , lelt(i; j; k), P  Q, A  B, a < b, bor(p; q), band(p; q), (i = j), P  Q, A, s = t, , b

Lemmas

eq int wf, band wf, bor wf, assert wf, bool wf, le int wf, lt int wf, bnot wf, assert of lt int, bnot of le int, true wf, squash wf, eqff to assert, iff transitivity, le wf, assert of le int, eqtt to assert, int seg wf, decidable assert, decidable int equal, decidable or, btrue wf, assert of band, assert of tt, assert of eq int, bfalse wf, assert of bor, decidable lt, sq stable from decidable, decidable le, sq stable and